A global constant is defined using the following syntax,

#define max 5;

#define is a keyword used for multiple purposes. Here it defines a global constant named max, which has the value 5. The semi-colon marks the end of the 'sentence'.

Note: the constant value can only be integer value (both positive and negative) and boolean value (true or false).

Service Channels

In WS module, service communication can be invoked between different roles. A service channel can be declared as follows.

channel c;

where channel is a key word for declaring channels only.

Propositions

In addition, the key word #define may be used to define propositions. For instance,

#define goal x == 0;

where goal is the name of the proposition and x == 0 is what goal means. A proposition name is used in the same way as global constant is used. For instance, given the above definition, we may write the following,

 if (goal) { P } else { Q };

which means if the value of x is 0 then do P else do Q. We remark that propositions are the basic elements of LTL formulae.